Inference at * 
Iof proof for Lemma dcdr-to-bool-equivalence:


  P:, d:Dec(P). ([d])  P 

latex

 by Auto 

latex

 1: 

 1: 1. P : 
 1: 2. d : Dec(P)
 1: 3. [d]
 1:   P
 2: 

 2: 1. P : 
 2: 2. d : Dec(P)
 2: 3. P
 2:   [d]
 .

Definitions	P  Q, P & Q, P  Q, P  Q, [d], b, Dec(P), x:A. B(x), t  T, , Type
Lemmas	assert wf, dcdr-to-bool wf, decidable wf